
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Backend.Lib.EData</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Backend.Lib.EData" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Backend.Lib.EData</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.CommonRuntime.html">Qcert.Common.CommonRuntime</a></span>.<br/>
<span class="kwd">Require</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html">Qcert.Utils.JSON</a></span>.<br/>
<span class="kwd">Require</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Data.DatatoJSON.html">Qcert.Common.Data.DatatoJSON</a></span>.<br/>
<span class="kwd">Require</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJavaScript.html">Qcert.Translation.NNRCtoJavaScript</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendModel.html">ErgoSpec.Backend.Model.ErgoBackendModel</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendRuntime.html">ErgoSpec.Backend.Model.ErgoBackendRuntime</a></span>.<br/>
<br/>
<span class="kwd">Module</span> <span class="id"><a name="EData">EData</a></span>(<span class="id">ergomodel</span>:<span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendModel.html#ErgoBackendModel">ErgoBackendModel</a></span>).<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.json">json</a></span> : <span class="kwd">Set</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html#json">JSON.json</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.data">data</a></span> : <span class="kwd">Set</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#data">Data.data</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.t">t</a></span> : <span class="kwd">Set</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span>.<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.jnil">jnil</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.json">json</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html#jnil">JSON.jnil</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.jnumber">jnumber</a></span> <span class="id">z</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.json">json</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html#jnumber">JSON.jnumber</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#z">z</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.jbool">jbool</a></span> <span class="id">b</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.json">json</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html#jbool">JSON.jbool</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#b">b</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.jstring">jstring</a></span> <span class="id">s</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.json">json</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html#jstring">JSON.jstring</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#s">s</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.jarray">jarray</a></span> <span class="id">jl</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.json">json</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html#jarray">JSON.jarray</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#jl">jl</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.jobject">jobject</a></span> <span class="id">jl</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.json">json</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html#jobject">JSON.jobject</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#jl">jl</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dunit">dunit</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dunit">Data.dunit</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dnat">dnat</a></span> <span class="id">z</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dnat">Data.dnat</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#z">z</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dfloat">dfloat</a></span> <span class="id">f</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dfloat">Data.dfloat</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#f">f</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dbool">dbool</a></span> <span class="id">b</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dbool">Data.dbool</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#b">b</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dstring">dstring</a></span> <span class="id">s</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dstring">Data.dstring</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#s">s</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dcoll">dcoll</a></span> <span class="id">dl</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dcoll">Data.dcoll</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#dl">dl</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.drec">drec</a></span> <span class="id">dl</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#drec">Data.drec</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#dl">dl</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dleft">dleft</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dleft">Data.dleft</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dright">dright</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dright">Data.dright</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dbrand">dbrand</a></span> <span class="id">b</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dbrand">Data.dbrand</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#b">b</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dsome">dsome</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dsome">Data.dsome</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dnone">dnone</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dnone">Data.dnone</a></span>.<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.dsuccess">dsuccess</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dleft">Data.dleft</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.derror">derror</a></span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span> -&gt; <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.data">data</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#dright">Data.dright</a></span>.<br/>
&nbsp;&nbsp;<br/>
<div class="doc">data -&gt; JSON *string* conversion </div>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.data_to_json_string">data_to_json_string</a></span> <span class="id">s</span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.DataModel.Data.html#data">Data.data</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#ergomodel.ergo_data_to_json_string">ergomodel.ergo_data_to_json_string</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#s">s</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="EData.json_to_json_string">json_to_json_string</a></span> <span class="id">s</span> : <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData.json">json</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.JSON.html#jsonToJS">JSON.jsonToJS</a></span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#s">s</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Lib.EData.html#EData">EData</a></span>.<br/>
<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
